%The  \emph{Equipes Associ\'ees} (EA) programme  of INRIA  aims at promoting and developing INRIA's international collaboration with high-level international research teams.  The programme paves the way for INRIA project-teams to create a strong scientific synergy and a common experience with foreign teams. 
FORCES (FORmalisms from Concurrency for Emergent Systems) is an ongoing project funded by %EA  and 
the  \emph{Equipes Associ\'ees} %(EA) 
programme  of INRIA. It is carried by the INRIA team COMETE (France), the IRCAM Music Representation Team %Research Group 
(France)  and the team AVISPA (Colombia). The main goal of FORCES is to provide  robust \emph{declarative formalisms} for modeling systems from emergent application areas of computer science in which our teams  have been working  during recent years: Namely, \emph{Security Protocols, Biological Systems} and \emph{Multimedia Semantic Interaction}. 

  \emph{Process calculi} are formalisms that treat communicating processes %(agents) 
much like the $\lambda$-calculus treats computable functions: The structure of terms reflects the structure of processes and process evolution is represented by  term reduction.   \emph{Concurrent Constraint Programming} (\ccp) based calculi \cite{semantic-ccp}  are computational models that combine the %traditional 
operational view of process calculi with a \emph{declarative} one based upon logic.
  
   Some of the members of FORCES developed and used \ntcc\ \cite{NPV02}, a timed \ccp\ calculus, to predict the behavior of 
%several 
systems from Security Protocols \cite{Olarte:08:SAC}, Systems Biology \cite{gutierrez07} and Multimedia Semantic Interaction \cite{rueda05}. Although these areas differ significantly from one another, there is a %fundamental 
crucial commonality in the %nature of the 
analysis we wanted to 
   perform %instead of achieve (CR)
    in them: \emph{Reachability} i.e., whether a system reaches a particular state.
%We chose \ntcc\  for these systems because it 
%In these systems, 
The \ntcc calculus provides several reasoning tools for reachability analysis.
These include %tools such as 
a temporal logic, a proof system, verification techniques, and a denotational semantics. 
%I think the following paragraph is intriguing: why a declared success was achieved with a non robust model?
% Despite the success of our applications of \ntcc\ to the above-mentioned areas, we have learned from our modeling experience and theoretical studies that \ntcc\ is not sufficiently robust for them. 
 % I propose the following (CR):
  
Nevertheless, we have learned from our modeling experience and theoretical studies that \ntcc\ is not sufficiently robust for these applications.  E.g., some security protocols use a mechanism to allow communication of \emph{nonces} (i.e., uniquely generated random number). The \ntcc\  calculus can at best express this mechanism indirectly \cite{Valencia05}. Also, \ntcc lacks 
%probabilistic/stochastic techniques. 
constructs for quantitative information, 
  %Models of many,  instead of The modeling of the...(CR)
which are essential for  biological systems.  %often require to cope with uncertain/approximate information %that can be... instead of which can then be....(CR)
%  that can be naturally represented using probabilistic/sto\-chas\-tic formalisms. 
Furthermore, we have identified 
musical settings exhibiting 
complex non-regular %temporal behavior of sound systems, instead of audio processing temporal behavior (CR)
   timed behavior %of sound systems 
that cannot be expressed in \ntcc.

 Our research strategy in FORCES has  been, with the benefit of hindsight, to develop declarative formalisms for modeling systems from the above-mentioned %emergent 
areas as suitable \emph{extensions} or \emph{specializations} of \ntcc. Our expertise in  \ntcc\ as well as our modeling experience in these areas have been fundamental for guiding our
research. 

This short paper provides an overview of FORCES. Further information  can be found at  \url{http://www.lix.polytechnique.fr/comete/Forces}. \\
 
